| Definitions | sumdeq(a;b), union-deq(A;B;a;b), locl(a), {T}, as @ bs, Y, eqof(d), p   q, reduce(f;k;as),  ,  , mk-ma, deq-member(eq;x;L), True, ff, tt, only members of L read x, k sends only on links in L, k affects only members of L, (precondition a:Outcome(p) is P:State(ds) -> Bool), f  g, with declarations ds:dsda:dak(v) sends f s v on link l, x : v, with declarations ds:dsda:daeffect of k(v) is x := f s v, only L sends on (l with tg), only members of L affect x :t, x : t initially x = v, , if b then t else f fi , t.2, t.1, rcv(l,tg), KindDeq, x  dom(f),   x. t(x), t T, Rsends?(x1), Reffect?(x1), P Q, R-base-ma(R), R-loc(R), @i: A, rcv(l,tg) declared in M, Rplus?(x1), Rnone?(x1),  b, P   Q,  x:A. B(x), P & Q, P  Q, False, x(s),  , a:A fp B(a), Unit,  A, Realizer, Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left right, Rnone(),  |